% INEQUALITIES with MINIMIUM and MAXIMUM on terms
% based on wsirs.tex paper 920303 thom fruehwirth
% 9310 Pascal Brisset ECRC

handler minmax.

option(already_in_store, on). 
option(already_in_heads, off).
option(check_guard_bindings, off).

	ground(X):- not nonground(X).

operator(700, xfx, lss).
operator(700, xfx, grt).
operator(700, xfx, neq).
operator(700, xfx, geq).
operator(700, xfx, leq).

constraints (leq)/2, (lss)/2, (neq)/2, minimum/3, maximum/3.

X geq Y :- Y leq X.
X grt Y :- Y lss X.


/* leq */

built_in     @ X leq Y <=> ground(X),ground(Y) | X @=< Y.
reflexivity  @ X leq X <=> true.

antisymmetry @ X leq Y, Y leq X <=> X = Y.

transitivity @ X leq Y, Y leq Z ==> X \== Y, Y \== Z, X \== Z | X leq Z.


/* lss */

built_in     @ X lss Y <=> ground(X),ground(Y) | X @< Y.
irreflexivity@ X lss X <=> fail.

subsumption  @ X lss Y \ X leq Y <=> true.

transitivity @ X lss Y, Y lss Z ==> X \== Y, Y \== Z | X lss Z.
transitivity @ X leq Y, Y lss Z ==> X \== Y, Y \== Z | X lss Z.
transitivity @ X lss Y, Y leq Z ==> X \== Y, Y \== Z | X lss Z.


/* neq */

built_in     @ X neq Y <=> X ~= Y | true.
irreflexivity@ X neq X <=> fail. 

subsumption  @ X neq Y \ Y neq X <=> true.
subsumption  @ X lss Y \ X neq Y <=> true.
subsumption  @ X lss Y \ Y neq X <=> true.

simplification @ X neq Y, X leq Y <=> X lss Y. 
simplification @ Y neq X, X leq Y <=> X lss Y. 



/* MINIMUM */

label_with minimum(X, Y, Z) if true.
minimum(X, Y, Z):- X leq Y, Z = X ; Y lss X, Z = Y.

built_in @ minimum(X, Y, Z) <=> ground(X),ground(Y) | (X@=<Y -> Z=X ; Z=Y).
built_in @ minimum(X, Y, Z) <=> Z~=X | Z = Y, Y lss X.
built_in @ minimum(Y, X, Z) <=> Z~=X | Z = Y, Y lss X.

min_eq @ minimum(X, X, Y) <=> X = Y.

min_leq @ Y leq X \ minimum(X, Y, Z) <=> Y=Z.
min_leq @ X leq Y \ minimum(X, Y, Z) <=> X=Z.
min_lss @ Z lss X \ minimum(X, Y, Z) <=> Y=Z.
min_lss @ Z lss Y \ minimum(X, Y, Z) <=> X=Z. 

functional @ minimum(X, Y, Z) \ minimum(X, Y, Z1) <=> Z1=Z.
functional @ minimum(X, Y, Z) \ minimum(Y, X, Z1) <=> Z1=Z.

propagation @ minimum(X, Y, Z) ==> X\==Y | Z leq X, Z leq Y.


/* MAXIMUM */

label_with maximum(X, Y, Z) if true.
maximum(X, Y, Z):- X leq Y, Z = Y ; Y lss X, Z = X.

built_in @ maximum(X, Y, Z) <=> ground(X),ground(Y) | (Y@=<X -> Z=X ; Z=Y).
built_in @ maximum(X, Y, Z) <=> Z~=X | Z = Y, X lss Y.
built_in @ maximum(Y, X, Z) <=> Z~=X | Z = Y, X lss Y.

max_eq @ maximum(X, X, Y) <=> X = Y.

max_leq @ Y leq X \ maximum(X, Y, Z) <=> X=Z.
max_leq @ X leq Y \ maximum(X, Y, Z) <=> Y=Z.
max_lss @ X lss Z \ maximum(X, Y, Z) <=> Y=Z.
max_lss @ Y lss Z \ maximum(X, Y, Z) <=> X=Z. 

functional @ maximum(X, Y, Z) \ maximum(X, Y, Z1) <=> Z1=Z.
functional @ maximum(X, Y, Z) \ maximum(Y, X, Z1) <=> Z1=Z.

propagation @ maximum(X, Y, Z) ==> X\==Y | X leq Z, Y leq Z.



% end of handler minmax